YES 2.9090000000000003
↳ HASKELL
↳ CR
((elemFM :: Int -> FiniteMap Int a -> Bool) :: Int -> FiniteMap Int a -> Bool) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
||||||||||||||||||||||||
elemFM :: Ord b => b -> FiniteMap b a -> Bool
|
||||||||||||||||||||||||
lookupFM :: Ord b => FiniteMap b a -> b -> Maybe a
|
import qualified FiniteMap import qualified Prelude |
case lookupFM fm key of Nothing → False Just elt → True
elemFM0 Nothing = False elemFM0 (Just elt) = True
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
((elemFM :: Int -> FiniteMap Int a -> Bool) :: Int -> FiniteMap Int a -> Bool) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
||||||||||||||||||||||||
elemFM :: Ord a => a -> FiniteMap a b -> Bool
|
||||||||||||||||||||||||
|
||||||||||||||||||||||||
lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((elemFM :: Int -> FiniteMap Int a -> Bool) :: Int -> FiniteMap Int a -> Bool) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
||||||||||||||||||||||||
elemFM :: Ord b => b -> FiniteMap b a -> Bool
|
||||||||||||||||||||||||
|
||||||||||||||||||||||||
lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b
|
import qualified FiniteMap import qualified Prelude |
lookupFM EmptyFM key = Nothing lookupFM (Branch key elt vw fm_l fm_r) key_to_find
| key_to_find < key
= lookupFM fm_l key_to_find | key_to_find > key
= lookupFM fm_r key_to_find | otherwise
= Just elt
lookupFM EmptyFM key = lookupFM4 EmptyFM key lookupFM (Branch key elt vw fm_l fm_r) key_to_find = lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find
lookupFM0 key elt vw fm_l fm_r key_to_find True = Just elt
lookupFM2 key elt vw fm_l fm_r key_to_find True = lookupFM fm_l key_to_find lookupFM2 key elt vw fm_l fm_r key_to_find False = lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key)
lookupFM1 key elt vw fm_l fm_r key_to_find True = lookupFM fm_r key_to_find lookupFM1 key elt vw fm_l fm_r key_to_find False = lookupFM0 key elt vw fm_l fm_r key_to_find otherwise
lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find = lookupFM2 key elt vw fm_l fm_r key_to_find (key_to_find < key)
lookupFM4 EmptyFM key = Nothing lookupFM4 wv ww = lookupFM3 wv ww
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
(elemFM :: Int -> FiniteMap Int a -> Bool) |
import qualified Maybe import qualified Prelude |
|||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||
elemFM :: Ord b => b -> FiniteMap b a -> Bool
|
|||||||||
|
|||||||||
lookupFM :: Ord b => FiniteMap b a -> b -> Maybe a
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
new_elemFM01(Branch(Neg(Succ(wx4000)), wx41, wx42, wx43, wx44), Neg(Zero), bb) → new_elemFM01(wx44, Neg(Zero), bb)
new_elemFM00(wx146, wx147, wx148, wx149, wx150, wx151, Succ(wx1520), Zero, ba) → new_elemFM01(wx150, Pos(Succ(wx151)), ba)
new_elemFM01(Branch(Pos(Succ(wx4000)), wx41, wx42, wx43, wx44), Pos(Succ(wx300)), bb) → new_elemFM0(wx4000, wx41, wx42, wx43, wx44, wx300, wx300, wx4000, bb)
new_elemFM01(Branch(Pos(Succ(wx4000)), wx41, wx42, wx43, wx44), Neg(Zero), bb) → new_elemFM01(wx43, Neg(Zero), bb)
new_elemFM01(Branch(Neg(Succ(wx4000)), wx41, wx42, wx43, wx44), Pos(Zero), bb) → new_elemFM01(wx44, Pos(Zero), bb)
new_elemFM00(wx146, wx147, wx148, wx149, wx150, wx151, Succ(wx1520), Succ(wx1530), ba) → new_elemFM00(wx146, wx147, wx148, wx149, wx150, wx151, wx1520, wx1530, ba)
new_elemFM01(Branch(Neg(Succ(wx4000)), wx41, wx42, wx43, wx44), Neg(Succ(wx300)), bb) → new_elemFM03(wx4000, wx41, wx42, wx43, wx44, wx300, wx4000, wx300, bb)
new_elemFM04(wx155, wx156, wx157, wx158, wx159, wx160, Succ(wx1610), Zero, bd) → new_elemFM01(wx159, Neg(Succ(wx160)), bd)
new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, Zero, Succ(wx800), bc) → new_elemFM01(wx76, Neg(Succ(wx78)), bc)
new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, Succ(wx700), Zero, h) → new_elemFM00(wx64, wx65, wx66, wx67, wx68, wx69, Succ(wx69), Succ(wx64), h)
new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, Succ(wx700), Succ(wx710), h) → new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, wx700, wx710, h)
new_elemFM04(wx155, wx156, wx157, wx158, wx159, wx160, Succ(wx1610), Succ(wx1620), bd) → new_elemFM04(wx155, wx156, wx157, wx158, wx159, wx160, wx1610, wx1620, bd)
new_elemFM01(Branch(Pos(Zero), wx41, wx42, wx43, wx44), Pos(Succ(wx300)), bb) → new_elemFM01(wx44, Pos(Succ(wx300)), bb)
new_elemFM01(Branch(Pos(Succ(wx4000)), wx41, wx42, wx43, wx44), Pos(Zero), bb) → new_elemFM01(wx43, Pos(Zero), bb)
new_elemFM01(Branch(Neg(wx400), wx41, wx42, wx43, wx44), Pos(Succ(wx300)), bb) → new_elemFM01(wx44, Pos(Succ(wx300)), bb)
new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, Succ(wx790), Zero, bc) → new_elemFM04(wx73, wx74, wx75, wx76, wx77, wx78, Succ(wx73), Succ(wx78), bc)
new_elemFM02(wx64, wx65, wx66, wx67, wx68, wx69, h) → new_elemFM00(wx64, wx65, wx66, wx67, wx68, wx69, Succ(wx69), Succ(wx64), h)
new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, Succ(wx790), Succ(wx800), bc) → new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, wx790, wx800, bc)
new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, Zero, Succ(wx710), h) → new_elemFM01(wx67, Pos(Succ(wx69)), h)
new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, Zero, Zero, bc) → new_elemFM05(wx73, wx74, wx75, wx76, wx77, wx78, bc)
new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, Zero, Zero, h) → new_elemFM02(wx64, wx65, wx66, wx67, wx68, wx69, h)
new_elemFM01(Branch(Neg(Zero), wx41, wx42, wx43, wx44), Neg(Succ(wx300)), bb) → new_elemFM01(wx43, Neg(Succ(wx300)), bb)
new_elemFM05(wx73, wx74, wx75, wx76, wx77, wx78, bc) → new_elemFM04(wx73, wx74, wx75, wx76, wx77, wx78, Succ(wx73), Succ(wx78), bc)
new_elemFM01(Branch(Pos(wx400), wx41, wx42, wx43, wx44), Neg(Succ(wx300)), bb) → new_elemFM01(wx43, Neg(Succ(wx300)), bb)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, Succ(wx790), Zero, bc) → new_elemFM04(wx73, wx74, wx75, wx76, wx77, wx78, Succ(wx73), Succ(wx78), bc)
new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, Succ(wx790), Succ(wx800), bc) → new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, wx790, wx800, bc)
new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, Zero, Zero, bc) → new_elemFM05(wx73, wx74, wx75, wx76, wx77, wx78, bc)
new_elemFM01(Branch(Neg(Succ(wx4000)), wx41, wx42, wx43, wx44), Neg(Succ(wx300)), bb) → new_elemFM03(wx4000, wx41, wx42, wx43, wx44, wx300, wx4000, wx300, bb)
new_elemFM01(Branch(Neg(Zero), wx41, wx42, wx43, wx44), Neg(Succ(wx300)), bb) → new_elemFM01(wx43, Neg(Succ(wx300)), bb)
new_elemFM04(wx155, wx156, wx157, wx158, wx159, wx160, Succ(wx1610), Zero, bd) → new_elemFM01(wx159, Neg(Succ(wx160)), bd)
new_elemFM03(wx73, wx74, wx75, wx76, wx77, wx78, Zero, Succ(wx800), bc) → new_elemFM01(wx76, Neg(Succ(wx78)), bc)
new_elemFM04(wx155, wx156, wx157, wx158, wx159, wx160, Succ(wx1610), Succ(wx1620), bd) → new_elemFM04(wx155, wx156, wx157, wx158, wx159, wx160, wx1610, wx1620, bd)
new_elemFM05(wx73, wx74, wx75, wx76, wx77, wx78, bc) → new_elemFM04(wx73, wx74, wx75, wx76, wx77, wx78, Succ(wx73), Succ(wx78), bc)
new_elemFM01(Branch(Pos(wx400), wx41, wx42, wx43, wx44), Neg(Succ(wx300)), bb) → new_elemFM01(wx43, Neg(Succ(wx300)), bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
new_elemFM01(Branch(Pos(Succ(wx4000)), wx41, wx42, wx43, wx44), Pos(Zero), bb) → new_elemFM01(wx43, Pos(Zero), bb)
new_elemFM01(Branch(Neg(Succ(wx4000)), wx41, wx42, wx43, wx44), Pos(Zero), bb) → new_elemFM01(wx44, Pos(Zero), bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
new_elemFM00(wx146, wx147, wx148, wx149, wx150, wx151, Succ(wx1520), Zero, ba) → new_elemFM01(wx150, Pos(Succ(wx151)), ba)
new_elemFM01(Branch(Pos(Succ(wx4000)), wx41, wx42, wx43, wx44), Pos(Succ(wx300)), bb) → new_elemFM0(wx4000, wx41, wx42, wx43, wx44, wx300, wx300, wx4000, bb)
new_elemFM01(Branch(Neg(wx400), wx41, wx42, wx43, wx44), Pos(Succ(wx300)), bb) → new_elemFM01(wx44, Pos(Succ(wx300)), bb)
new_elemFM02(wx64, wx65, wx66, wx67, wx68, wx69, h) → new_elemFM00(wx64, wx65, wx66, wx67, wx68, wx69, Succ(wx69), Succ(wx64), h)
new_elemFM00(wx146, wx147, wx148, wx149, wx150, wx151, Succ(wx1520), Succ(wx1530), ba) → new_elemFM00(wx146, wx147, wx148, wx149, wx150, wx151, wx1520, wx1530, ba)
new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, Zero, Succ(wx710), h) → new_elemFM01(wx67, Pos(Succ(wx69)), h)
new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, Zero, Zero, h) → new_elemFM02(wx64, wx65, wx66, wx67, wx68, wx69, h)
new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, Succ(wx700), Zero, h) → new_elemFM00(wx64, wx65, wx66, wx67, wx68, wx69, Succ(wx69), Succ(wx64), h)
new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, Succ(wx700), Succ(wx710), h) → new_elemFM0(wx64, wx65, wx66, wx67, wx68, wx69, wx700, wx710, h)
new_elemFM01(Branch(Pos(Zero), wx41, wx42, wx43, wx44), Pos(Succ(wx300)), bb) → new_elemFM01(wx44, Pos(Succ(wx300)), bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
new_elemFM01(Branch(Neg(Succ(wx4000)), wx41, wx42, wx43, wx44), Neg(Zero), bb) → new_elemFM01(wx44, Neg(Zero), bb)
new_elemFM01(Branch(Pos(Succ(wx4000)), wx41, wx42, wx43, wx44), Neg(Zero), bb) → new_elemFM01(wx43, Neg(Zero), bb)
From the DPs we obtained the following set of size-change graphs: